YES 18.216 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((maximum :: [Float ->  Float) :: [Float ->  Float)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((maximum :: [Float ->  Float) :: [Float ->  Float)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
max x y
 | x <= y
 = y
 | otherwise
 = x

is transformed to
max x y = max2 x y

max0 x y True = x

max1 x y True = y
max1 x y False = max0 x y otherwise

max2 x y = max1 x y (x <= y)

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (maximum :: [Float ->  Float)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vx4400), Succ(vx3100000)) → new_primPlusNat(vx4400, vx3100000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vx300000), vx310000) → new_primMulNat(vx300000, vx310000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat0(Succ(vx2000), Succ(vx2200)) → new_primMulNat0(vx2000, Succ(vx2200))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_not(Succ(vx37800), Succ(vx40700)) → new_not(vx37800, vx40700)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldl(vx30, :(vx310, vx311)) → new_foldl(new_max1(vx30, vx310), vx311)

The TRS R consists of the following rules:

new_max176(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max146(Float(Pos(Zero), Neg(Succ(vx310100))), new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max156(vx19, Neg(Succ(vx2000)), vx21, Pos(Zero), Zero) → new_max115(vx19, vx2000, vx21, new_not9(Zero))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max1107(vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max130(vx14, Neg(Succ(vx1500)), vx16, Pos(Succ(vx1700)), Zero) → new_max17(vx14, vx1500, vx16, vx1700, new_not7(new_primPlusNat1(new_primMulNat2(vx1500, Succ(vx1700)), Succ(vx1700))))
new_max198(vx310000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Succ(vx310000)), Pos(Zero))
new_max15(vx19, vx21, True) → Float(Neg(Succ(vx21)), Neg(Zero))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Succ(vx310000)), Pos(Zero))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max12(vx30000, vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max139(vx30000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_primMulNat1(Zero, vx310000) → Zero
new_max1144(vx14, vx1500, vx16, False) → new_max01(vx14, Succ(vx1500), vx16, Zero)
new_max19(vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max11(vx3010000, vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max130(vx14, Neg(Zero), vx16, Neg(Zero), Succ(vx450)) → new_max1151(vx14, vx16, new_not11(vx450))
new_max130(vx14, Neg(Zero), vx16, Neg(Succ(vx1700)), Zero) → new_max1143(vx14, vx16, vx1700, new_not6(Zero))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max18(vx30000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1131(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max193(vx30000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max1124(vx310000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1166(vx35, vx360, vx37, vx380, True) → Float(Neg(Succ(vx37)), Neg(vx380))
new_max121(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Zero)))
new_max181(vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max144(vx310000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Zero)))
new_max130(vx14, Neg(Succ(vx1500)), vx16, Neg(Succ(vx1700)), Zero) → new_max1149(vx14, vx1500, vx16, vx1700, new_not6(new_primPlusNat1(new_primMulNat2(vx1500, Succ(vx1700)), Succ(vx1700))))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max144(vx310000, vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1118(vx30000, vx3010000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_max130(vx14, Neg(Zero), vx16, Pos(Succ(vx1700)), Zero) → new_max14(vx14, vx16, vx1700, new_not7(Zero))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Pos(Zero), Pos(Zero)))
new_max163(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_not8(Zero) → new_not10
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1101(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max116(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1161(vx30, vx310, vx32, vx330, False) → Float(Neg(Succ(vx30)), Pos(vx310))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max145(vx3010000, Float(Pos(Succ(vx310000)), Pos(Succ(vx310100))), new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max145(vx100, vx11, True) → vx11
new_max130(vx14, Pos(Succ(vx1500)), vx16, Neg(Succ(vx1700)), Zero) → new_max1152(vx14, vx1500, vx16, vx1700, new_not7(new_primPlusNat1(new_primMulNat2(vx1500, Succ(vx1700)), Succ(vx1700))))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Neg(Succ(vx30000)), Neg(Succ(vx30100))))
new_max130(vx14, Pos(Zero), vx16, Neg(Zero), Zero) → new_max1154(vx14, vx16, new_not7(Zero))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max152(vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1168(vx19, vx21, vx2200, False) → Float(Pos(Succ(vx19)), Neg(Zero))
new_max164(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Zero)))
new_max170(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max118(vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max199(vx310000, vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Pos(Zero), Pos(Succ(vx30100))))
new_max1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Pos(Succ(vx30000)), Pos(Zero)))
new_max137(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max140(vx3010000, vx310000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1164(vx35, vx360, vx37, vx380, True) → Float(Neg(Succ(vx37)), Pos(vx380))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max139(vx30000, vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max130(vx14, Neg(vx150), vx16, Pos(vx170), Succ(vx450)) → new_max0(vx14, vx150, vx16, vx170)
new_max1(Float(Pos(Zero), Neg(Succ(Succ(vx301000)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max175(vx301000, Float(Neg(Zero), Neg(Succ(vx310100))), vx310100)
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max1126(vx310000, vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max149(vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max138(vx30000, vx3010000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1170(vx19, vx21, vx2200, True) → Float(Neg(Succ(vx21)), Neg(Succ(vx2200)))
new_max10(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max130(vx14, Pos(Zero), vx16, Pos(Zero), Zero) → new_max1148(vx14, vx16, new_not6(Zero))
new_max1115(vx30000, vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max1138(vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1118(vx30000, vx3010000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1146(vx14, vx1500, vx16, True) → Float(Pos(Succ(vx16)), Pos(Zero))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max153(vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max196(vx310000, vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_not11(vx450) → new_not3
new_max1143(vx14, vx16, vx1700, False) → Float(Pos(Succ(vx14)), Neg(Zero))
new_max130(vx14, Pos(Succ(vx1500)), vx16, Pos(Zero), Zero) → new_max1146(vx14, vx1500, vx16, new_not6(Zero))
new_max1137(vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1155(vx14, vx1500, vx16, True) → Float(Pos(Succ(vx16)), Pos(Zero))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max1105(vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max120(vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max170(vx310000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max1127(vx3010000, vx310000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max189(vx30000, vx3010000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max188(vx30000, vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max179(vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max188(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Zero)))
new_max111(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Zero)))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max171(vx310000, vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1120(vx30000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max141(vx310000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Pos(Succ(vx30000)), Pos(Succ(vx30100))))
new_max190(vx30000, vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1153(vx14, vx16, vx1700, True) → Float(Pos(Succ(vx16)), Neg(Succ(vx1700)))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max1122(vx30000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max130(vx14, Pos(Succ(vx1500)), vx16, Pos(Succ(vx1700)), Zero) → new_max1145(vx14, vx1500, vx16, vx1700, new_not6(new_primPlusNat1(new_primMulNat2(vx1500, Succ(vx1700)), Succ(vx1700))))
new_max192(vx30000, vx3010000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1169(vx19, vx2000, vx21, vx2200, True) → Float(Neg(Succ(vx21)), Neg(Succ(vx2200)))
new_max1118(vx30000, vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max192(vx30000, vx3010000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max132(vx30000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Succ(vx310000)), Neg(Zero))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max14(vx14, vx16, vx1700, False) → new_max0(vx14, Zero, vx16, Succ(vx1700))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Succ(vx310000)), Neg(Zero))
new_max184(vx310100, False) → Float(Pos(Zero), Neg(Succ(Zero)))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max162(vx30000, vx3010000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max167(vx30000, vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max143(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max184(vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max154(vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max158(vx30000, vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max169(vx3010000, vx310000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max115(vx19, vx2000, vx21, True) → Float(Neg(Succ(vx21)), Pos(Zero))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max1103(vx310000, vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max197(vx3010000, vx310000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max130(vx14, Neg(Zero), vx16, Neg(Succ(vx1700)), Succ(vx450)) → new_max1143(vx14, vx16, vx1700, new_not11(vx450))
new_max136(vx30000, vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1141(vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max130(vx14, Pos(vx150), vx16, Neg(vx170), Succ(vx450)) → new_max01(vx14, vx150, vx16, vx170)
new_max130(vx14, Neg(Zero), vx16, Neg(Zero), Zero) → new_max1151(vx14, vx16, new_not6(Zero))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_not5new_not0
new_max1134(vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1119(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_max1168(vx19, vx21, vx2200, True) → Float(Neg(Succ(vx21)), Pos(Succ(vx2200)))
new_max156(vx19, Pos(Succ(vx2000)), vx21, Neg(Zero), Succ(vx1410)) → new_max1158(vx19, vx2000, vx21, new_not13(Zero, vx1410))
new_max1114(vx30000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max1136(vx3010000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1116(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max187(vx30000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max134(vx30000, vx3010000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1123(vx3010000, vx310000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Succ(vx310000)), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Succ(vx310000)), Neg(Zero))
new_max1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Succ(vx310000)), Neg(Zero))
new_max1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Succ(vx310000)), Pos(Zero))
new_max178(vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max1142(vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max154(vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max1130(vx3010000, vx310000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max11(vx3010000, vx310000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1158(vx19, vx2000, vx21, True) → Float(Neg(Succ(vx21)), Neg(Zero))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max1137(vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max118(vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max156(vx19, Pos(Succ(vx2000)), vx21, Neg(Zero), Zero) → new_max1158(vx19, vx2000, vx21, new_not9(Zero))
new_max1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Neg(Zero), Neg(Succ(vx30100))))
new_max1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Neg(Succ(vx30000)), Neg(Zero)))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max149(vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max156(vx19, Pos(Succ(vx2000)), vx21, Neg(Succ(vx2200)), Zero) → new_max1169(vx19, vx2000, vx21, vx2200, new_not9(new_primPlusNat1(new_primMulNat2(vx2000, Succ(vx2200)), Succ(vx2200))))
new_primMulNat2(Zero, Zero) → Zero
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max13(vx30000, vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max1115(vx30000, vx3010000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max193(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_max197(vx3010000, vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max179(vx310100, False) → Float(Pos(Zero), Pos(Succ(Zero)))
new_max167(vx30000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max130(vx14, Pos(Succ(vx1500)), vx16, Pos(Zero), Succ(vx450)) → new_max1146(vx14, vx1500, vx16, new_not11(vx450))
new_max1124(vx310000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_max185(vx30, Pos(vx310), vx32, Pos(vx330), Succ(vx2540)) → new_max1162(vx30, vx310, vx32, vx330, new_not4(vx2540, vx310, vx330))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max146(Float(Pos(Zero), Pos(Succ(vx310100))), new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max14(vx14, vx16, vx1700, True) → Float(Pos(Succ(vx16)), Pos(Succ(vx1700)))
new_max199(vx310000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Zero)))
new_max183(vx310100, False) → Float(Pos(Zero), Neg(Succ(Zero)))
new_max1119(vx30000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max162(vx30000, vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Succ(vx310000)), Neg(Zero))
new_max153(vx310100, False) → Float(Pos(Zero), Pos(Succ(Zero)))
new_not3False
new_max161(vx8) → Float(Neg(Zero), Neg(Zero))
new_max194(vx3010000, vx310000, vx310100, False) → new_max00(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), vx310000, vx310100)
new_max155(vx310100, False) → Float(Pos(Zero), Neg(Succ(Zero)))
new_max160(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_max1100(vx3010000, vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), vx301), Float(Neg(Succ(vx310000)), vx3101)) → new_max1111(vx30000, vx301, vx310000, vx3101, new_primPlusNat1(new_primMulNat2(vx30000, Succ(vx310000)), Succ(vx310000)))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max138(vx30000, vx3010000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max185(vx30, Neg(vx310), vx32, Pos(vx330), Succ(vx2540)) → new_max1163(vx30, vx310, vx32, vx330, new_not12(vx2540, new_primMulNat2(vx310, vx330)))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max190(vx30000, vx3010000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Succ(vx310000)), Pos(Zero))
new_max1163(vx30, vx310, vx32, vx330, True) → Float(Pos(Succ(vx32)), Pos(vx330))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max112(vx310000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max157(vx30000, vx3010000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max147(vx310000, vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1159(vx19, vx2000, vx21, vx2200, False) → Float(Pos(Succ(vx19)), Neg(Succ(vx2000)))
new_max132(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_max1(Float(Pos(Succ(vx30000)), vx301), Float(Pos(Succ(vx310000)), vx3101)) → new_max130(vx30000, vx301, vx310000, vx3101, new_primPlusNat0(new_primMulNat1(vx30000, vx310000), vx310000))
new_max137(vx30000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1132(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max150(vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max1104(vx3010000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max165(vx30000, vx3010000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max173(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1161(vx30, vx310, vx32, vx330, True) → Float(Pos(Succ(vx32)), Neg(vx330))
new_max11(vx3010000, vx310000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max113(vx3010000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max152(vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max125(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Zero)))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max1129(vx310000, vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max18(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_max185(vx30, Pos(vx310), vx32, Pos(vx330), Zero) → new_max1162(vx30, vx310, vx32, vx330, new_not8(new_primMulNat2(vx310, vx330)))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max176(vx310000, vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1103(vx310000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Zero)))
new_max165(vx30000, vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1135(vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Pos(Succ(vx30000)), vx301), Float(Neg(Succ(vx310000)), vx3101)) → new_max156(vx30000, vx301, vx310000, vx3101, new_primPlusNat1(new_primMulNat1(vx30000, vx310000), Succ(vx310000)))
new_max110(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_max148(vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max120(vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max172(vx3010000, vx310000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max113(vx3010000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max138(vx30000, vx3010000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max10(vx310000, vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1120(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Zero)))
new_max1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1111(vx35, Neg(vx360), vx37, Neg(vx380), Succ(vx3780)) → new_max1166(vx35, vx360, vx37, vx380, new_not1(vx3780, new_primMulNat2(vx360, vx380)))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max145(vx3010000, Float(Pos(Zero), Pos(Succ(vx310100))), new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1112(vx30000, vx3010000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max158(vx30000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max166(vx30000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max119(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Zero)))
new_max156(vx19, Neg(vx200), vx21, Neg(vx220), Succ(vx1410)) → new_max1167(vx19, vx200, vx21, vx220, new_not4(vx1410, vx200, vx220))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max195(vx310000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1129(vx310000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Zero)))
new_max174(vx310000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Zero)))
new_max1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Succ(vx310000)), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Succ(vx310000)), Pos(Zero))
new_max146(vx11, True) → vx11
new_primMulNat1(Succ(vx300000), vx310000) → new_primPlusNat0(new_primMulNat1(vx300000, vx310000), vx310000)
new_primPlusNat0(Succ(vx440), vx310000) → Succ(Succ(new_primPlusNat1(vx440, vx310000)))
new_max126(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max110(vx30000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max1141(vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1143(vx14, vx16, vx1700, True) → Float(Pos(Succ(vx16)), Neg(Succ(vx1700)))
new_max156(vx19, Pos(vx200), vx21, Pos(vx220), Zero) → new_max1160(vx19, vx200, vx21, vx220, new_not8(new_primMulNat2(vx200, vx220)))
new_max1109(vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max163(vx30000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max19(vx3010000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max136(vx30000, vx3010000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_max160(vx30000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max145(vx3010000, Float(Neg(Succ(vx310000)), Pos(Succ(vx310100))), new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max148(vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1150(vx14, vx1500, vx16, False) → Float(Pos(Succ(vx14)), Neg(Succ(vx1500)))
new_max13(vx30000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max146(Float(Pos(Succ(vx310000)), Neg(Succ(vx310100))), new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max115(vx19, vx2000, vx21, False) → Float(Pos(Succ(vx19)), Neg(Succ(vx2000)))
new_max185(vx30, Neg(vx310), vx32, Neg(vx330), Zero) → new_max123(vx30, vx310, vx32, vx330, new_not8(new_primMulNat2(vx310, vx330)))
new_max133(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Zero)))
new_max1127(vx3010000, vx310000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max157(vx30000, vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), vx301), Float(Pos(Succ(vx310000)), vx3101)) → new_max185(vx30000, vx301, vx310000, vx3101, new_primPlusNat1(new_primMulNat2(vx30000, Succ(vx310000)), Succ(vx310000)))
new_max10(vx310000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Zero)))
new_primPlusNat1(Succ(vx4400), Zero) → Succ(vx4400)
new_primPlusNat1(Zero, Succ(vx3100000)) → Succ(vx3100000)
new_max167(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Zero)))
new_max1105(vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max119(vx30000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1152(vx14, vx1500, vx16, vx1700, True) → Float(Pos(Succ(vx16)), Neg(Succ(vx1700)))
new_max1133(vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max134(vx30000, vx3010000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1116(vx30000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1134(vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1142(vx310100, False) → Float(Neg(Zero), Neg(Succ(Zero)))
new_max175(Zero, vx11, vx12) → new_max146(vx11, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx12)), Succ(vx12))))
new_max1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1163(vx30, vx310, vx32, vx330, False) → Float(Neg(Succ(vx30)), Neg(vx310))
new_max1104(vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Succ(vx310000)), Neg(Zero))
new_max1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Succ(vx310000)), Neg(Zero))
new_max1158(vx19, vx2000, vx21, False) → Float(Pos(Succ(vx19)), Pos(Succ(vx2000)))
new_max190(vx30000, vx3010000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_not7(Succ(vx4160)) → new_not3
new_not4(vx1410, vx200, vx220) → new_not5
new_max185(vx30, Pos(vx310), vx32, Neg(vx330), Zero) → new_max1161(vx30, vx310, vx32, vx330, new_not9(new_primMulNat2(vx310, vx330)))
new_max158(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Zero)))
new_max1128(vx310000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_max130(vx14, Neg(Succ(vx1500)), vx16, Neg(Zero), Succ(vx450)) → new_max1150(vx14, vx1500, vx16, new_not11(vx450))
new_not9(Zero) → new_not10
new_max1148(vx14, vx16, False) → Float(Pos(Succ(vx14)), Pos(Zero))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Succ(vx310000)), Pos(Zero))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max185(vx30, Neg(vx310), vx32, Neg(vx330), Succ(vx2540)) → new_max123(vx30, vx310, vx32, vx330, new_not4(vx2540, vx310, vx330))
new_max1127(vx3010000, vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max19(vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max178(vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1113(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max1121(vx30000, vx3010000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max168(vx5, False) → Float(Pos(Succ(vx5)), Neg(Zero))
new_max114(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_max1128(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max170(vx310000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_max1117(vx30000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max196(vx310000, vx310100, False) → new_max00(Float(Neg(Zero), Pos(Succ(Zero))), vx310000, vx310100)
new_max117(vx3010000, vx310000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max156(vx19, Pos(Zero), vx21, Neg(Succ(vx2200)), Succ(vx1410)) → new_max1170(vx19, vx21, vx2200, new_not13(Zero, vx1410))
new_max1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Succ(vx310000)), Neg(Zero))
new_not7(Zero) → new_not10
new_not2(Succ(vx37800), Succ(vx40700)) → new_not2(vx37800, vx40700)
new_max1162(vx30, vx310, vx32, vx330, True) → Float(Pos(Succ(vx32)), Pos(vx330))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1113(vx30000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max17(vx14, vx1500, vx16, vx1700, False) → new_max0(vx14, Succ(vx1500), vx16, Succ(vx1700))
new_max1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Succ(vx310000)), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1111(vx35, Pos(vx360), vx37, Pos(vx380), Succ(vx3780)) → new_max1164(vx35, vx360, vx37, vx380, new_not1(vx3780, new_primMulNat2(vx360, vx380)))
new_max1156(vx35, vx360, vx37, vx380, False) → Float(Neg(Succ(vx35)), Neg(vx360))
new_max1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Succ(vx310000)), Neg(Zero))
new_max1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max1117(vx30000, vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max151(vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max1123(vx3010000, vx310000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max155(vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1170(vx19, vx21, vx2200, False) → Float(Pos(Succ(vx19)), Pos(Zero))
new_not1(vx3780, Zero) → new_not3
new_max197(vx3010000, vx310000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max134(vx30000, vx3010000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_max118(vx310100, False) → Float(Neg(Zero), Neg(Succ(Zero)))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max1109(vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max160(vx30000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max128(vx310000, vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max150(vx310100, False) → Float(Pos(Zero), Pos(Succ(Zero)))
new_max1151(vx14, vx16, True) → Float(Pos(Succ(vx16)), Neg(Zero))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1133(vx3010000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max150(vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max189(vx30000, vx3010000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_not1(vx3780, Succ(vx4070)) → new_not2(vx3780, vx4070)
new_max193(vx30000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max180(vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max151(vx3010000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max159(vx30000, vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Neg(Zero), Pos(Succ(vx30100))))
new_max1(Float(Neg(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Neg(Succ(vx30000)), Pos(Zero)))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1114(vx30000, vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Pos(Zero), Neg(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Pos(Zero), Neg(Succ(vx30100))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max117(vx3010000, vx310000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max171(vx310000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Zero)))
new_max1152(vx14, vx1500, vx16, vx1700, False) → new_max01(vx14, Succ(vx1500), vx16, Succ(vx1700))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max191(vx30000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1167(vx19, vx200, vx21, vx220, False) → Float(Pos(Succ(vx19)), Neg(vx200))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max1131(vx310000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max186(vx30000, vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max149(vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_max130(vx14, Neg(Zero), vx16, Pos(Zero), Zero) → new_max129(vx14, vx16, new_not7(Zero))
new_max166(vx30000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max147(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max139(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Zero)))
new_max0(vx14, vx150, vx16, vx170) → Float(Pos(Succ(vx14)), Neg(vx150))
new_max125(vx30000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max148(vx3010000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max156(vx19, Pos(vx200), vx21, Pos(vx220), Succ(vx1410)) → new_max1160(vx19, vx200, vx21, vx220, new_not4(vx1410, vx200, vx220))
new_max1103(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max112(vx310000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_max1131(vx310000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max172(vx3010000, vx310000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max116(vx310000, vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max129(vx14, vx16, False) → new_max0(vx14, Zero, vx16, Zero)
new_max140(vx3010000, vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1144(vx14, vx1500, vx16, True) → Float(Pos(Succ(vx16)), Neg(Zero))
new_max153(vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max156(vx19, Neg(Zero), vx21, Pos(Succ(vx2200)), Zero) → new_max1168(vx19, vx21, vx2200, new_not9(Zero))
new_max1148(vx14, vx16, True) → Float(Pos(Succ(vx16)), Pos(Zero))
new_max130(vx14, Pos(Zero), vx16, Pos(Succ(vx1700)), Succ(vx450)) → new_max1147(vx14, vx16, vx1700, new_not11(vx450))
new_max1157(vx19, vx21, False) → Float(Pos(Succ(vx19)), Neg(Zero))
new_max1132(vx310000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Zero)))
new_max1114(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Zero)))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max186(vx30000, vx3010000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max183(vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(vx301000)))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max175(vx301000, Float(Neg(Succ(vx310000)), Neg(Succ(vx310100))), vx310100)
new_primPlusNat1(Succ(vx4400), Succ(vx3100000)) → Succ(Succ(new_primPlusNat1(vx4400, vx3100000)))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max1132(vx310000, vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1138(vx310100, False) → Float(Neg(Zero), Pos(Succ(Zero)))
new_max1111(vx35, Pos(vx360), vx37, Pos(vx380), Zero) → new_max1164(vx35, vx360, vx37, vx380, new_not6(new_primMulNat2(vx360, vx380)))
new_max142(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max145(vx100, vx11, False) → Float(Pos(Zero), Neg(Succ(Succ(Succ(vx100)))))
new_max156(vx19, Pos(Succ(vx2000)), vx21, Neg(Succ(vx2200)), Succ(vx1410)) → new_max1169(vx19, vx2000, vx21, vx2200, new_not13(new_primPlusNat1(new_primMulNat2(vx2000, Succ(vx2200)), Succ(vx2200)), vx1410))
new_max1(Float(Pos(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Neg(Zero))) → new_max168(vx30000, new_not8(Zero))
new_max174(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_primMulNat2(Succ(vx2000), Zero) → Zero
new_primMulNat2(Zero, Succ(vx2200)) → Zero
new_not12(vx2540, vx286) → new_not13(vx286, vx2540)
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max1101(vx310000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max1128(vx310000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1122(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_max195(vx310000, vx310100, False) → new_max00(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), vx310000, vx310100)
new_max135(vx30000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1121(vx30000, vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_not10new_not0
new_max152(vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max133(vx30000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max121(vx30000, vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max164(vx30000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1133(vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max127(vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max130(vx14, Pos(Zero), vx16, Pos(Zero), Succ(vx450)) → new_max1148(vx14, vx16, new_not11(vx450))
new_max01(vx14, vx150, vx16, vx170) → Float(Pos(Succ(vx14)), Pos(vx150))
new_max130(vx14, Pos(Zero), vx16, Neg(Succ(vx1700)), Zero) → new_max1153(vx14, vx16, vx1700, new_not7(Zero))
new_max1162(vx30, vx310, vx32, vx330, False) → Float(Neg(Succ(vx30)), Pos(vx310))
new_max1129(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max130(vx14, Pos(Succ(vx1500)), vx16, Neg(Zero), Zero) → new_max1144(vx14, vx1500, vx16, new_not7(Zero))
new_max187(vx30000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_primPlusNat0(Zero, vx310000) → Succ(vx310000)
new_max1138(vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max156(vx19, Neg(Succ(vx2000)), vx21, Pos(Succ(vx2200)), Zero) → new_max1159(vx19, vx2000, vx21, vx2200, new_not9(new_primPlusNat1(new_primMulNat2(vx2000, Succ(vx2200)), Succ(vx2200))))
new_max1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max111(vx30000, vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max179(vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_not2(Zero, Zero) → new_not10
new_not6(Zero) → new_not10
new_max1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Pos(Succ(vx310000)), Pos(Zero))) → Float(Pos(Succ(vx310000)), Pos(Zero))
new_max1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Pos(Succ(vx310100)))) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max169(vx3010000, vx310000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max181(vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max130(vx14, Pos(Succ(vx1500)), vx16, Pos(Succ(vx1700)), Succ(vx450)) → new_max1145(vx14, vx1500, vx16, vx1700, new_not2(Succ(vx450), new_primPlusNat1(new_primMulNat2(vx1500, Succ(vx1700)), Succ(vx1700))))
new_not0True
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max126(vx310000, vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max121(vx30000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1123(vx3010000, vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max165(vx30000, vx3010000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_max166(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Neg(Zero), Neg(Zero)))
new_max113(vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max136(vx30000, vx3010000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1109(vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max15(vx19, vx21, False) → Float(Pos(Succ(vx19)), Pos(Zero))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max00(vx563, vx564, vx565) → vx563
new_max1104(vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1135(vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1110(vx310100, False) → Float(Neg(Zero), Neg(Succ(Zero)))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max1108(vx3010000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max123(vx30, vx310, vx32, vx330, False) → Float(Neg(Succ(vx30)), Neg(vx310))
new_max169(vx3010000, vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max1102(vx3010000, vx310000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_not2(Succ(vx37800), Zero) → new_not3
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max159(vx30000, vx3010000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max174(vx310000, vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1100(vx3010000, vx310000, vx310100, False) → new_max00(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), vx310000, vx310100)
new_max1125(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max186(vx30000, vx3010000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_max143(vx310000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_max198(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max1116(vx30000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_not9(Succ(vx1610)) → new_not11(vx1610)
new_max194(vx3010000, vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), Pos(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Neg(Succ(vx30000)), Pos(Succ(vx30100))))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(vx30100))), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Pos(Succ(vx30000)), Neg(Succ(vx30100))))
new_max131(vx30000, vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max16(vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1102(vx3010000, vx310000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1160(vx19, vx200, vx21, vx220, False) → Float(Pos(Succ(vx19)), Pos(vx200))
new_max156(vx19, Pos(Zero), vx21, Neg(Zero), Zero) → new_max15(vx19, vx21, new_not9(Zero))
new_max132(vx30000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max163(vx30000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max196(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max180(vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1153(vx14, vx16, vx1700, False) → new_max01(vx14, Zero, vx16, Succ(vx1700))
new_max175(Succ(vx100), vx11, vx12) → new_max145(vx100, vx11, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx100, Succ(vx12)), Succ(vx12)), Succ(vx12)), Succ(vx12))))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max185(vx30, Pos(vx310), vx32, Neg(vx330), Succ(vx2540)) → new_max1161(vx30, vx310, vx32, vx330, new_not12(vx2540, new_primMulNat2(vx310, vx330)))
new_max17(vx14, vx1500, vx16, vx1700, True) → Float(Pos(Succ(vx16)), Pos(Succ(vx1700)))
new_max162(vx30000, vx3010000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max145(vx3010000, Float(Pos(Succ(vx310000)), Neg(Succ(vx310100))), new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max135(vx30000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1139(vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_max110(vx30000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max146(Float(Neg(Zero), Pos(Succ(vx310100))), new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1124(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max141(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1111(vx35, Pos(vx360), vx37, Neg(vx380), Zero) → new_max1165(vx35, vx360, vx37, vx380, new_not7(new_primMulNat2(vx360, vx380)))
new_max1140(vx310100, False) → Float(Neg(Zero), Neg(Succ(Zero)))
new_max1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Succ(vx310000)), Neg(Zero))
new_max1(Float(Pos(Succ(vx30000)), Pos(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Succ(vx30100))), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Succ(vx310000)), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max192(vx30000, vx3010000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1121(vx30000, vx3010000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1136(vx3010000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1135(vx310100, False) → Float(Neg(Zero), Pos(Succ(Zero)))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max146(Float(Pos(Succ(vx310000)), Pos(Succ(vx310100))), new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1165(vx35, vx360, vx37, vx380, False) → Float(Neg(Succ(vx35)), Pos(vx360))
new_max188(vx30000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1111(vx35, Pos(vx360), vx37, Neg(vx380), Succ(vx3780)) → new_max1165(vx35, vx360, vx37, vx380, new_not14(vx3780, new_primMulNat2(vx360, vx380)))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max133(vx30000, vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1167(vx19, vx200, vx21, vx220, True) → Float(Neg(Succ(vx21)), Neg(vx220))
new_max1108(vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1165(vx35, vx360, vx37, vx380, True) → Float(Neg(Succ(vx37)), Neg(vx380))
new_max1149(vx14, vx1500, vx16, vx1700, True) → Float(Pos(Succ(vx16)), Neg(Succ(vx1700)))
new_max181(vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_max1112(vx30000, vx3010000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1107(vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1112(vx30000, vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max168(vx5, True) → Float(Neg(Zero), Neg(Zero))
new_max1149(vx14, vx1500, vx16, vx1700, False) → Float(Pos(Succ(vx14)), Neg(Succ(vx1500)))
new_max112(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max157(vx30000, vx3010000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_max144(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max155(vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1151(vx14, vx16, False) → Float(Pos(Succ(vx14)), Neg(Zero))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1142(vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max172(vx3010000, vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_not2(Zero, Succ(vx40700)) → new_not5
new_max1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Pos(Zero))) → Float(Pos(Zero), Pos(Zero))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max146(Float(Neg(Succ(vx310000)), Pos(Succ(vx310100))), new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1154(vx14, vx16, True) → Float(Pos(Succ(vx16)), Neg(Zero))
new_max182(vx310100, False) → Float(Pos(Zero), Pos(Succ(Zero)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Succ(vx310100)))) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Neg(Zero))) → Float(Neg(Succ(vx310000)), Neg(Zero))
new_max1154(vx14, vx16, False) → new_max01(vx14, Zero, vx16, Zero)
new_max146(vx11, False) → Float(Pos(Zero), Neg(Succ(Succ(Zero))))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1140(vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max1125(vx310000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max128(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1126(vx310000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Zero)))
new_not6(Succ(vx3920)) → new_not13(Zero, vx3920)
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max199(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Succ(vx310000)), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Succ(vx30100))), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Succ(vx310000)), Neg(Zero))
new_max1(Float(Neg(Succ(vx30000)), Neg(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_not13(Zero, vx1410) → new_not5
new_not14(vx3780, vx415) → new_not3
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max159(vx30000, vx3010000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(vx30100))), Float(Pos(Zero), Neg(Zero))) → Float(Pos(Zero), Neg(Zero))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(vx30100))), Float(Neg(Zero), Pos(Zero))) → Float(Neg(Zero), Pos(Zero))
new_max141(vx310000, vx310100, False) → new_max00(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), vx310000, vx310100)
new_max1101(vx310000, vx310100, False) → new_max00(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), vx310000, vx310100)
new_max1107(vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_max114(vx30000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max178(vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max143(vx310000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max191(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero))))
new_max1111(vx35, Neg(vx360), vx37, Pos(vx380), Succ(vx3780)) → new_max1156(vx35, vx360, vx37, vx380, new_not14(vx3780, new_primMulNat2(vx360, vx380)))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max1100(vx3010000, vx310000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Succ(vx310000)), Neg(Zero))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Succ(vx310000)), Pos(Zero))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max135(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_max1147(vx14, vx16, vx1700, False) → new_max00(Float(Pos(Succ(vx14)), Pos(Zero)), vx16, vx1700)
new_max129(vx14, vx16, True) → Float(Pos(Succ(vx16)), Pos(Zero))
new_max12(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Neg(Succ(Zero)))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max1110(vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max177(vx3010000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1125(vx310000, vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_max1160(vx19, vx200, vx21, vx220, True) → Float(Neg(Succ(vx21)), Pos(vx220))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max125(vx30000, vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max177(vx3010000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1119(vx30000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_not13(Succ(vx1860), vx1410) → new_not2(vx1860, vx1410)
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max180(vx3010000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max164(vx30000, vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max116(vx310000, vx310100, False) → new_max00(Float(Neg(Zero), Neg(Succ(Zero))), vx310000, vx310100)
new_max191(vx30000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max156(vx19, Pos(Zero), vx21, Neg(Succ(vx2200)), Zero) → new_max1170(vx19, vx21, vx2200, new_not9(Zero))
new_max130(vx14, Neg(Succ(vx1500)), vx16, Pos(Zero), Zero) → new_max1155(vx14, vx1500, vx16, new_not7(Zero))
new_max1110(vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1105(vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_max1155(vx14, vx1500, vx16, False) → new_max0(vx14, Succ(vx1500), vx16, Zero)
new_max1164(vx35, vx360, vx37, vx380, False) → Float(Neg(Succ(vx35)), Pos(vx360))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max182(vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max151(vx3010000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max194(vx3010000, vx310000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max137(vx30000, vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1140(vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max156(vx19, Neg(Zero), vx21, Pos(Zero), Zero) → new_max1157(vx19, vx21, new_not9(Zero))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max131(vx30000, vx3010000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max13(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Neg(Succ(Zero)))
new_max1146(vx14, vx1500, vx16, False) → Float(Pos(Succ(vx14)), Pos(Succ(vx1500)))
new_max156(vx19, Pos(Zero), vx21, Neg(Zero), Succ(vx1410)) → new_max15(vx19, vx21, new_not13(Zero, vx1410))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max184(vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1108(vx3010000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1111(vx35, Neg(vx360), vx37, Pos(vx380), Zero) → new_max1156(vx35, vx360, vx37, vx380, new_not7(new_primMulNat2(vx360, vx380)))
new_max1134(vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → new_max142(vx310000, vx310100, new_not6(new_primPlusNat1(Zero, Succ(vx310100))))
new_max124(vx30000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1145(vx14, vx1500, vx16, vx1700, True) → Float(Pos(Succ(vx16)), Pos(Succ(vx1700)))
new_max189(vx30000, vx3010000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1157(vx19, vx21, True) → Float(Neg(Succ(vx21)), Pos(Zero))
new_max1115(vx30000, vx3010000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Neg(Succ(vx30000)), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1120(vx30000, vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1159(vx19, vx2000, vx21, vx2200, True) → Float(Neg(Succ(vx21)), Pos(Succ(vx2200)))
new_max1147(vx14, vx16, vx1700, True) → Float(Pos(Succ(vx16)), Pos(Succ(vx1700)))
new_max182(vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1122(vx30000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max1139(vx310100, new_not7(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max145(vx3010000, Float(Pos(Zero), Neg(Succ(vx310100))), new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max111(vx30000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1150(vx14, vx1500, vx16, True) → Float(Pos(Succ(vx16)), Neg(Zero))
new_max156(vx19, Neg(Zero), vx21, Pos(Succ(vx2200)), Succ(vx1410)) → new_max1168(vx19, vx21, vx2200, new_not13(Zero, vx1410))
new_max127(vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1145(vx14, vx1500, vx16, vx1700, False) → new_max00(Float(Pos(Succ(vx14)), Pos(Succ(vx1500))), vx16, vx1700)
new_not8(Succ(vx1840)) → new_not5
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max183(vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max12(vx30000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max177(vx3010000, vx310100, new_not8(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max130(vx14, Neg(Succ(vx1500)), vx16, Neg(Zero), Zero) → new_max1150(vx14, vx1500, vx16, new_not6(Zero))
new_max1106(vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max156(vx19, Neg(vx200), vx21, Neg(vx220), Zero) → new_max1167(vx19, vx200, vx21, vx220, new_not8(new_primMulNat2(vx200, vx220)))
new_max122(vx3010000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1166(vx35, vx360, vx37, vx380, False) → Float(Neg(Succ(vx35)), Neg(vx360))
new_primPlusNat1(Zero, Zero) → Zero
new_max123(vx30, vx310, vx32, vx330, True) → Float(Pos(Succ(vx32)), Neg(vx330))
new_max1106(vx310100, False) → Float(Neg(Zero), Pos(Succ(Zero)))
new_max173(vx310000, vx310100, False) → Float(Pos(Zero), Pos(Succ(Succ(Zero))))
new_max117(vx3010000, vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max187(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Succ(Zero))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Zero))) → new_max161(Float(Pos(Zero), Neg(Zero)))
new_max130(vx14, Neg(Succ(vx1500)), vx16, Neg(Succ(vx1700)), Succ(vx450)) → new_max1149(vx14, vx1500, vx16, vx1700, new_not2(Succ(vx450), new_primPlusNat1(new_primMulNat2(vx1500, Succ(vx1700)), Succ(vx1700))))
new_max1117(vx30000, vx310100, False) → Float(Neg(Succ(vx30000)), Pos(Succ(Zero)))
new_max176(vx310000, vx310100, False) → Float(Pos(Zero), Neg(Succ(Zero)))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max119(vx30000, vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1137(vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max173(vx310000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Pos(Succ(vx310100)))) → new_max145(vx3010000, Float(Neg(Zero), Pos(Succ(vx310100))), new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max195(vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max120(vx310100, False) → Float(Neg(Zero), Pos(Succ(Succ(Zero))))
new_max185(vx30, Neg(vx310), vx32, Pos(vx330), Zero) → new_max1163(vx30, vx310, vx32, vx330, new_not9(new_primMulNat2(vx310, vx330)))
new_max126(vx310000, vx310100, False) → Float(Pos(Zero), Neg(Succ(Zero)))
new_max154(vx310100, False) → Float(Pos(Zero), Neg(Succ(Zero)))
new_max1156(vx35, vx360, vx37, vx380, True) → Float(Neg(Succ(vx37)), Pos(vx380))
new_max124(vx30000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Zero)))
new_max1139(vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))) → Float(Pos(Succ(vx310000)), Pos(Succ(vx310100)))
new_max1141(vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Zero))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max122(vx3010000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1130(vx3010000, vx310000, vx310100, False) → Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Succ(vx310000)), Pos(Zero))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Succ(vx310000)), Neg(Zero))
new_primMulNat2(Succ(vx2000), Succ(vx2200)) → new_primPlusNat1(new_primMulNat2(vx2000, Succ(vx2200)), Succ(vx2200))
new_max1102(vx3010000, vx310000, vx310100, True) → Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))
new_max130(vx14, Pos(Zero), vx16, Pos(Succ(vx1700)), Zero) → new_max1147(vx14, vx16, vx1700, new_not6(Zero))
new_max131(vx30000, vx3010000, vx310100, False) → Float(Pos(Succ(vx30000)), Pos(Succ(Succ(Succ(vx3010000)))))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max1106(vx310100, new_not9(new_primPlusNat1(Zero, Succ(vx310100))))
new_max18(vx30000, vx310100, True) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1111(vx35, Neg(vx360), vx37, Neg(vx380), Zero) → new_max1166(vx35, vx360, vx37, vx380, new_not6(new_primMulNat2(vx360, vx380)))
new_max156(vx19, Neg(Zero), vx21, Pos(Zero), Succ(vx1410)) → new_max1157(vx19, vx21, new_not13(Zero, vx1410))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Succ(vx310000)), Pos(Zero))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Succ(vx310000)), Neg(Zero))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Succ(vx310100)))) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(vx310000)), Neg(Zero))) → Float(Pos(Succ(vx310000)), Neg(Zero))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Succ(vx310100)))) → Float(Pos(Zero), Neg(Succ(vx310100)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(vx310000)), Pos(Zero))) → Float(Neg(Succ(vx310000)), Pos(Zero))
new_max140(vx3010000, vx310000, vx310100, False) → new_max00(Float(Pos(Zero), Pos(Succ(Succ(Succ(vx3010000))))), vx310000, vx310100)
new_max122(vx3010000, vx310100, True) → Float(Pos(Zero), Pos(Succ(vx310100)))
new_max128(vx310000, vx310100, False) → Float(Pos(Zero), Neg(Succ(Zero)))
new_max1126(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max1(Float(Pos(Succ(vx30000)), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max124(vx30000, vx310100, new_not7(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1136(vx3010000, vx310100, True) → Float(Neg(Zero), Neg(Succ(vx310100)))
new_max147(vx310000, vx310100, False) → new_max00(Float(Pos(Zero), Neg(Succ(Zero))), vx310000, vx310100)
new_max1169(vx19, vx2000, vx21, vx2200, False) → Float(Pos(Succ(vx19)), Pos(Succ(vx2000)))
new_max156(vx19, Neg(Succ(vx2000)), vx21, Pos(Succ(vx2200)), Succ(vx1410)) → new_max1159(vx19, vx2000, vx21, vx2200, new_not13(new_primPlusNat1(new_primMulNat2(vx2000, Succ(vx2200)), Succ(vx2200)), vx1410))
new_max16(vx310100, False) → Float(Neg(Zero), Pos(Succ(Zero)))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(vx310100)))) → new_max16(vx310100, new_not8(new_primPlusNat1(Zero, Succ(vx310100))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(vx310000)), Neg(Succ(vx310100)))) → new_max198(vx310000, vx310100, new_not9(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max142(vx310000, vx310100, False) → new_max00(Float(Pos(Zero), Pos(Succ(Zero))), vx310000, vx310100)
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(vx3010000))))), Float(Neg(Zero), Neg(Succ(vx310100)))) → new_max127(vx3010000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(new_primPlusNat1(new_primMulNat2(vx3010000, Succ(vx310100)), Succ(vx310100)), Succ(vx310100)), Succ(vx310100))))
new_max1113(vx30000, vx310100, True) → Float(Neg(Zero), Pos(Succ(vx310100)))
new_max156(vx19, Neg(Succ(vx2000)), vx21, Pos(Zero), Succ(vx1410)) → new_max115(vx19, vx2000, vx21, new_not13(Zero, vx1410))
new_max1(Float(Pos(Succ(vx30000)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(vx310100)))) → new_max114(vx30000, vx310100, new_not6(new_primPlusNat1(new_primPlusNat1(Zero, Succ(vx310100)), Succ(vx310100))))
new_max1130(vx3010000, vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Neg(Succ(vx310100)))
new_max171(vx310000, vx310100, True) → Float(Neg(Succ(vx310000)), Pos(Succ(vx310100)))

The set Q consists of the following terms:

new_not11(x0)
new_not7(Zero)
new_max1120(x0, x1, False)
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x1))))
new_max1125(x0, x1, False)
new_max1108(x0, x1, False)
new_max123(x0, x1, x2, x3, False)
new_max1143(x0, x1, x2, True)
new_max177(x0, x1, False)
new_max182(x0, True)
new_max1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Succ(x0))), Float(Neg(Succ(x1)), Neg(Zero)))
new_max197(x0, x1, x2, True)
new_max196(x0, x1, False)
new_max1156(x0, x1, x2, x3, True)
new_max1163(x0, x1, x2, x3, True)
new_max121(x0, x1, False)
new_max1140(x0, False)
new_max153(x0, True)
new_max152(x0, True)
new_max1(Float(Pos(Zero), Neg(Succ(Succ(x0)))), Float(Neg(Succ(x1)), Neg(Succ(x2))))
new_max1100(x0, x1, x2, False)
new_max188(x0, x1, True)
new_max178(x0, False)
new_max1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Pos(Zero)))
new_max1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Pos(Zero)))
new_max1105(x0, True)
new_max1140(x0, True)
new_max170(x0, x1, False)
new_max1133(x0, x1, False)
new_max179(x0, False)
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Zero)))
new_max1158(x0, x1, x2, True)
new_max128(x0, x1, True)
new_max1170(x0, x1, x2, True)
new_max1150(x0, x1, x2, True)
new_primPlusNat0(Zero, x0)
new_max1138(x0, True)
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Succ(x0))), Float(Neg(Succ(x1)), Pos(Zero)))
new_max1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Succ(x0))), Float(Pos(Succ(x1)), Neg(Zero)))
new_max1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x1))))
new_max189(x0, x1, x2, True)
new_max1(Float(Pos(Zero), Neg(Succ(x0))), Float(Neg(Succ(x1)), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(x0))), Float(Neg(Succ(x1)), Neg(Zero)))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x1))))
new_max1145(x0, x1, x2, x3, True)
new_max19(x0, x1, True)
new_max1127(x0, x1, x2, False)
new_max155(x0, True)
new_max1111(x0, Pos(x1), x2, Pos(x3), Zero)
new_max176(x0, x1, True)
new_max1111(x0, Pos(x1), x2, Pos(x3), Succ(x4))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max00(x0, x1, x2)
new_max1136(x0, x1, True)
new_max1100(x0, x1, x2, True)
new_max1132(x0, x1, True)
new_max192(x0, x1, x2, False)
new_max1124(x0, x1, True)
new_max1154(x0, x1, True)
new_max1160(x0, x1, x2, x3, False)
new_max15(x0, x1, False)
new_max1148(x0, x1, False)
new_max13(x0, x1, True)
new_max13(x0, x1, False)
new_max1102(x0, x1, x2, True)
new_max1(Float(Neg(Zero), Neg(Succ(x0))), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Pos(Succ(x2))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Pos(Succ(x2))))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Pos(Succ(x2))))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Neg(Succ(x2))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Neg(Succ(x1))))
new_max1117(x0, x1, False)
new_max157(x0, x1, x2, False)
new_max196(x0, x1, True)
new_max136(x0, x1, x2, True)
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Neg(Zero)))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Pos(Zero)))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Pos(Zero)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Pos(Zero)))
new_max127(x0, x1, True)
new_max155(x0, False)
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x1))))
new_not13(Zero, x0)
new_max129(x0, x1, True)
new_primMulNat2(Succ(x0), Zero)
new_max187(x0, x1, False)
new_max181(x0, False)
new_max1118(x0, x1, x2, True)
new_max130(x0, Pos(Succ(x1)), x2, Pos(Succ(x3)), Zero)
new_max179(x0, True)
new_primPlusNat0(Succ(x0), x1)
new_max159(x0, x1, x2, True)
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1153(x0, x1, x2, False)
new_max122(x0, x1, False)
new_max1166(x0, x1, x2, x3, True)
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_max126(x0, x1, True)
new_max115(x0, x1, x2, True)
new_max1129(x0, x1, True)
new_max1164(x0, x1, x2, x3, True)
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max151(x0, x1, True)
new_max1109(x0, True)
new_max1(Float(Neg(Succ(x0)), Neg(Succ(x1))), Float(Neg(Zero), Neg(Zero)))
new_max130(x0, Pos(Succ(x1)), x2, Pos(Zero), Zero)
new_max130(x0, Neg(Succ(x1)), x2, Pos(Zero), Zero)
new_max130(x0, Pos(Succ(x1)), x2, Neg(Zero), Zero)
new_max1111(x0, Neg(x1), x2, Pos(x3), Zero)
new_max1111(x0, Pos(x1), x2, Neg(x3), Zero)
new_max165(x0, x1, x2, True)
new_not1(x0, Zero)
new_max191(x0, x1, False)
new_max1116(x0, x1, False)
new_max117(x0, x1, x2, False)
new_max183(x0, False)
new_max158(x0, x1, False)
new_max1126(x0, x1, True)
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Succ(x0))))
new_max130(x0, Neg(Succ(x1)), x2, Neg(Succ(x3)), Zero)
new_max1117(x0, x1, True)
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Succ(x0))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Succ(x0))))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Succ(x0))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Succ(x0))))
new_max1155(x0, x1, x2, True)
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_primPlusNat1(Zero, Succ(x0))
new_max150(x0, False)
new_max1147(x0, x1, x2, True)
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Zero)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Zero)))
new_max1165(x0, x1, x2, x3, True)
new_max1161(x0, x1, x2, x3, False)
new_max148(x0, x1, True)
new_max186(x0, x1, x2, False)
new_max114(x0, x1, False)
new_max12(x0, x1, True)
new_max173(x0, x1, False)
new_max1111(x0, Neg(x1), x2, Pos(x3), Succ(x4))
new_max1111(x0, Pos(x1), x2, Neg(x3), Succ(x4))
new_max169(x0, x1, x2, True)
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Neg(Succ(x2))))
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Pos(Succ(x2))))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Neg(Succ(x2))))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Pos(Succ(x2))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Pos(Succ(x2))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Neg(Succ(x2))))
new_max175(Succ(x0), x1, x2)
new_max1134(x0, False)
new_max10(x0, x1, True)
new_max14(x0, x1, x2, True)
new_max184(x0, False)
new_max11(x0, x1, x2, True)
new_max0(x0, x1, x2, x3)
new_max192(x0, x1, x2, True)
new_max1144(x0, x1, x2, False)
new_max143(x0, x1, True)
new_max113(x0, x1, True)
new_max1156(x0, x1, x2, x3, False)
new_max1130(x0, x1, x2, False)
new_max140(x0, x1, x2, False)
new_max130(x0, Pos(Zero), x1, Neg(Zero), Zero)
new_max130(x0, Neg(Zero), x1, Pos(Zero), Zero)
new_max130(x0, Pos(Zero), x1, Pos(Zero), Zero)
new_max1137(x0, True)
new_max119(x0, x1, True)
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Neg(Succ(x2))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Neg(Succ(x2))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Pos(Succ(x2))))
new_max153(x0, False)
new_max1144(x0, x1, x2, True)
new_max156(x0, Neg(Zero), x1, Pos(Zero), Zero)
new_max156(x0, Pos(Zero), x1, Neg(Zero), Zero)
new_max188(x0, x1, False)
new_max189(x0, x1, x2, False)
new_max1152(x0, x1, x2, x3, True)
new_max19(x0, x1, False)
new_max1122(x0, x1, False)
new_max167(x0, x1, True)
new_max132(x0, x1, True)
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Zero)))
new_max140(x0, x1, x2, True)
new_max112(x0, x1, False)
new_max149(x0, True)
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x1))))
new_max1165(x0, x1, x2, x3, False)
new_max1124(x0, x1, False)
new_max16(x0, True)
new_max1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Neg(Zero)))
new_max132(x0, x1, False)
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Succ(x0))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Succ(x0))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Succ(x0))))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Succ(x0))))
new_max1112(x0, x1, x2, True)
new_max146(x0, True)
new_max110(x0, x1, True)
new_max186(x0, x1, x2, True)
new_max1159(x0, x1, x2, x3, True)
new_max1128(x0, x1, False)
new_not4(x0, x1, x2)
new_max115(x0, x1, x2, False)
new_max173(x0, x1, True)
new_max165(x0, x1, x2, False)
new_max160(x0, x1, True)
new_not6(Zero)
new_not13(Succ(x0), x1)
new_max142(x0, x1, False)
new_max182(x0, False)
new_max1(Float(Pos(Zero), Pos(Succ(x0))), Float(Pos(Zero), Pos(Zero)))
new_max125(x0, x1, True)
new_max1130(x0, x1, x2, True)
new_max1(Float(Pos(Succ(x0)), x1), Float(Pos(Succ(x2)), x3))
new_max171(x0, x1, True)
new_max130(x0, Neg(Zero), x1, Neg(Succ(x2)), Succ(x3))
new_max185(x0, Pos(x1), x2, Pos(x3), Succ(x4))
new_max185(x0, Pos(x1), x2, Neg(x3), Succ(x4))
new_max185(x0, Neg(x1), x2, Pos(x3), Succ(x4))
new_max168(x0, False)
new_max1168(x0, x1, x2, True)
new_max130(x0, Pos(x1), x2, Neg(x3), Succ(x4))
new_max130(x0, Neg(x1), x2, Pos(x3), Succ(x4))
new_max154(x0, True)
new_max191(x0, x1, True)
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1104(x0, x1, False)
new_max18(x0, x1, False)
new_max1104(x0, x1, True)
new_max128(x0, x1, False)
new_max156(x0, Neg(Zero), x1, Pos(Zero), Succ(x2))
new_max156(x0, Pos(Zero), x1, Neg(Zero), Succ(x2))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Neg(Zero)))
new_max1169(x0, x1, x2, x3, False)
new_max141(x0, x1, True)
new_max1123(x0, x1, x2, False)
new_max172(x0, x1, x2, False)
new_max1(Float(Neg(Zero), Neg(Succ(x0))), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Neg(Zero), Neg(Succ(x0))), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Pos(Zero), Neg(Succ(x0))), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Neg(Zero), Pos(Succ(x0))), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Pos(Zero)))
new_max1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Pos(Zero)))
new_max184(x0, True)
new_max1118(x0, x1, x2, False)
new_max134(x0, x1, x2, False)
new_max130(x0, Neg(Zero), x1, Neg(Succ(x2)), Zero)
new_max113(x0, x1, False)
new_not12(x0, x1)
new_max183(x0, True)
new_max190(x0, x1, x2, True)
new_max1168(x0, x1, x2, False)
new_max14(x0, x1, x2, False)
new_max1133(x0, x1, True)
new_max126(x0, x1, False)
new_max136(x0, x1, x2, False)
new_max168(x0, True)
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x0))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x0))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x0))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x0))))
new_primPlusNat1(Zero, Zero)
new_not0
new_max147(x0, x1, True)
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x0))))
new_max156(x0, Neg(Succ(x1)), x2, Pos(Zero), Succ(x3))
new_max156(x0, Pos(Succ(x1)), x2, Neg(Zero), Succ(x3))
new_max169(x0, x1, x2, False)
new_max125(x0, x1, False)
new_max163(x0, x1, True)
new_max185(x0, Neg(x1), x2, Pos(x3), Zero)
new_max1121(x0, x1, x2, True)
new_max185(x0, Pos(x1), x2, Neg(x3), Zero)
new_max199(x0, x1, True)
new_max1135(x0, False)
new_max130(x0, Neg(Succ(x1)), x2, Neg(Zero), Zero)
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1131(x0, x1, False)
new_max156(x0, Pos(Zero), x1, Neg(Succ(x2)), Zero)
new_max156(x0, Neg(Zero), x1, Pos(Succ(x2)), Zero)
new_max138(x0, x1, x2, False)
new_max195(x0, x1, False)
new_max1119(x0, x1, False)
new_max145(x0, x1, False)
new_max1143(x0, x1, x2, False)
new_max1152(x0, x1, x2, x3, False)
new_max151(x0, x1, False)
new_max1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Pos(Succ(x0))), Float(Pos(Succ(x1)), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Pos(Succ(x0))), Float(Neg(Succ(x1)), Pos(Zero)))
new_max1(Float(Pos(Zero), Neg(Succ(x0))), Float(Pos(Succ(x1)), Pos(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(x0))), Float(Pos(Succ(x1)), Pos(Zero)))
new_max1162(x0, x1, x2, x3, False)
new_max1116(x0, x1, True)
new_max1164(x0, x1, x2, x3, False)
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Pos(Succ(x2))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Pos(Succ(x2))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Pos(Succ(x2))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Neg(Succ(x2))))
new_max1107(x0, False)
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max137(x0, x1, False)
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max166(x0, x1, True)
new_max120(x0, False)
new_max1101(x0, x1, False)
new_max1106(x0, False)
new_max124(x0, x1, False)
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1106(x0, True)
new_max1(Float(Neg(Succ(x0)), Pos(Succ(x1))), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(x1))), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(x1))), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(x1))), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(x1))), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Neg(Succ(x0)), Neg(Succ(x1))), Float(Pos(Zero), Pos(Zero)))
new_max194(x0, x1, x2, True)
new_max139(x0, x1, True)
new_max116(x0, x1, True)
new_max141(x0, x1, False)
new_primPlusNat1(Succ(x0), Succ(x1))
new_max133(x0, x1, True)
new_not3
new_primPlusNat1(Succ(x0), Zero)
new_max156(x0, Neg(x1), x2, Neg(x3), Zero)
new_max1(Float(Pos(Succ(x0)), x1), Float(Neg(Succ(x2)), x3))
new_max1(Float(Neg(Succ(x0)), x1), Float(Pos(Succ(x2)), x3))
new_max144(x0, x1, False)
new_max156(x0, Neg(Succ(x1)), x2, Pos(Succ(x3)), Zero)
new_max156(x0, Pos(Succ(x1)), x2, Neg(Succ(x3)), Zero)
new_max12(x0, x1, False)
new_max130(x0, Pos(Succ(x1)), x2, Neg(Succ(x3)), Zero)
new_max130(x0, Neg(Succ(x1)), x2, Pos(Succ(x3)), Zero)
new_max133(x0, x1, False)
new_max197(x0, x1, x2, False)
new_max156(x0, Neg(x1), x2, Neg(x3), Succ(x4))
new_max185(x0, Neg(x1), x2, Neg(x3), Zero)
new_max131(x0, x1, x2, True)
new_max1(Float(Neg(Zero), Pos(Succ(x0))), Float(Neg(Succ(x1)), Pos(Zero)))
new_max1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(x0))), Float(Pos(Succ(x1)), Neg(Zero)))
new_max1(Float(Neg(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(x0))), Float(Pos(Succ(x1)), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(x0))), Float(Neg(Succ(x1)), Pos(Zero)))
new_max1(Float(Pos(Zero), Pos(Succ(x0))), Float(Neg(Succ(x1)), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Neg(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Succ(x0))), Float(Pos(Succ(x1)), Pos(Zero)))
new_max1147(x0, x1, x2, False)
new_max119(x0, x1, False)
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x0))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x0))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x0))))
new_max139(x0, x1, False)
new_max120(x0, True)
new_not6(Succ(x0))
new_max149(x0, False)
new_max1132(x0, x1, False)
new_max130(x0, Pos(Zero), x1, Pos(Succ(x2)), Succ(x3))
new_max172(x0, x1, x2, True)
new_max1149(x0, x1, x2, x3, True)
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x0))))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x0))))
new_not2(Succ(x0), Succ(x1))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Neg(Succ(x2))))
new_max138(x0, x1, x2, True)
new_max147(x0, x1, False)
new_max123(x0, x1, x2, x3, True)
new_max1102(x0, x1, x2, False)
new_max143(x0, x1, False)
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1145(x0, x1, x2, x3, False)
new_max1111(x0, Neg(x1), x2, Neg(x3), Zero)
new_not5
new_max1157(x0, x1, True)
new_max1141(x0, True)
new_not2(Succ(x0), Zero)
new_max180(x0, x1, True)
new_max1(Float(Neg(Succ(x0)), Neg(Succ(x1))), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Neg(Succ(x0)), Neg(Succ(x1))), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(x1))), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(x1))), Float(Neg(Zero), Neg(Zero)))
new_max1158(x0, x1, x2, False)
new_max122(x0, x1, True)
new_max1(Float(Pos(Zero), Pos(Succ(x0))), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Pos(Zero), Pos(Succ(x0))), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Pos(Zero), Neg(Succ(x0))), Float(Pos(Zero), Pos(Zero)))
new_max1(Float(Neg(Zero), Pos(Succ(x0))), Float(Pos(Zero), Pos(Zero)))
new_max150(x0, True)
new_primMulNat2(Zero, Zero)
new_max1107(x0, True)
new_max1103(x0, x1, True)
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Pos(Succ(x2))))
new_max1161(x0, x1, x2, x3, True)
new_max1167(x0, x1, x2, x3, False)
new_max166(x0, x1, False)
new_max1142(x0, False)
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x0))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x0))))
new_max1148(x0, x1, True)
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x0))))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x0))))
new_max15(x0, x1, True)
new_max175(Zero, x0, x1)
new_max1146(x0, x1, x2, False)
new_max10(x0, x1, False)
new_max1146(x0, x1, x2, True)
new_max187(x0, x1, True)
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Pos(Zero)))
new_not2(Zero, Succ(x0))
new_max167(x0, x1, False)
new_max193(x0, x1, True)
new_max1111(x0, Neg(x1), x2, Neg(x3), Succ(x4))
new_max1115(x0, x1, x2, True)
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Pos(Zero)))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Neg(Zero)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Neg(Zero)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Pos(Zero)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Pos(Zero)))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Neg(Zero)))
new_not9(Succ(x0))
new_max1123(x0, x1, x2, True)
new_max11(x0, x1, x2, False)
new_not14(x0, x1)
new_max185(x0, Neg(x1), x2, Neg(x3), Succ(x4))
new_max1151(x0, x1, True)
new_max193(x0, x1, False)
new_max130(x0, Neg(Succ(x1)), x2, Neg(Zero), Succ(x3))
new_max18(x0, x1, True)
new_max148(x0, x1, False)
new_max131(x0, x1, x2, False)
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1169(x0, x1, x2, x3, True)
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1166(x0, x1, x2, x3, False)
new_max130(x0, Pos(Succ(x1)), x2, Pos(Succ(x3)), Succ(x4))
new_primMulNat1(Succ(x0), x1)
new_max1142(x0, True)
new_max16(x0, False)
new_max146(x0, False)
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Pos(Zero), Neg(Succ(x2))))
new_max1(Float(Pos(Zero), Pos(Succ(x0))), Float(Pos(Succ(x1)), Pos(Zero)))
new_max1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Neg(Succ(x2))))
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Pos(Succ(x2))))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Neg(Succ(x2))))
new_max1121(x0, x1, x2, False)
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1103(x0, x1, False)
new_max118(x0, False)
new_max156(x0, Neg(Zero), x1, Pos(Succ(x2)), Succ(x3))
new_max156(x0, Pos(Zero), x1, Neg(Succ(x2)), Succ(x3))
new_max1113(x0, x1, True)
new_max1120(x0, x1, True)
new_primMulNat2(Succ(x0), Succ(x1))
new_max144(x0, x1, True)
new_max117(x0, x1, x2, True)
new_max1170(x0, x1, x2, False)
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1131(x0, x1, True)
new_max1134(x0, True)
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Pos(Zero)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Succ(x0)), Neg(Zero)))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Succ(x0))), Float(Pos(Zero), Pos(Zero)))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Succ(x0)), Neg(Zero)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Neg(Zero)))
new_max1(Float(Pos(Zero), Pos(Succ(x0))), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(x0))), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Pos(Zero), Neg(Succ(x0))), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Neg(Zero), Pos(Succ(x0))), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Neg(Zero), Pos(Succ(x0))), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(x1))), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(x1))), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(x1))), Float(Pos(Zero), Pos(Zero)))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(x1))), Float(Pos(Zero), Pos(Zero)))
new_not8(Succ(x0))
new_max159(x0, x1, x2, False)
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Neg(Zero), Neg(Zero)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Pos(Zero), Neg(Zero)))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Zero), Pos(Zero)))
new_max1135(x0, True)
new_max1159(x0, x1, x2, x3, False)
new_max1141(x0, False)
new_max194(x0, x1, x2, False)
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x0))))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x0))))
new_max1(Float(Neg(Zero), Neg(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x0))))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Neg(Zero), Neg(Succ(x0))))
new_max1137(x0, False)
new_max1129(x0, x1, False)
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Pos(Succ(x2))))
new_max130(x0, Pos(Zero), x1, Pos(Zero), Succ(x2))
new_max160(x0, x1, False)
new_max198(x0, x1, False)
new_max116(x0, x1, False)
new_max111(x0, x1, False)
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x1))))
new_max1108(x0, x1, True)
new_max145(x0, x1, True)
new_max177(x0, x1, True)
new_max110(x0, x1, False)
new_max1115(x0, x1, x2, False)
new_max129(x0, x1, False)
new_max1155(x0, x1, x2, False)
new_max1153(x0, x1, x2, True)
new_max130(x0, Pos(Zero), x1, Pos(Succ(x2)), Zero)
new_max180(x0, x1, False)
new_not2(Zero, Zero)
new_max181(x0, True)
new_max1127(x0, x1, x2, True)
new_max1110(x0, True)
new_max176(x0, x1, False)
new_max1113(x0, x1, False)
new_max156(x0, Pos(Succ(x1)), x2, Neg(Zero), Zero)
new_max156(x0, Neg(Succ(x1)), x2, Pos(Zero), Zero)
new_max185(x0, Pos(x1), x2, Pos(x3), Zero)
new_max1151(x0, x1, False)
new_max170(x0, x1, True)
new_max1163(x0, x1, x2, x3, False)
new_max17(x0, x1, x2, x3, False)
new_max127(x0, x1, False)
new_max1160(x0, x1, x2, x3, True)
new_max174(x0, x1, True)
new_max1162(x0, x1, x2, x3, True)
new_max111(x0, x1, True)
new_primMulNat1(Zero, x0)
new_max1(Float(Neg(Succ(x0)), Neg(Zero)), Float(Neg(Zero), Neg(Zero)))
new_max1128(x0, x1, True)
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x0))))
new_max1157(x0, x1, False)
new_max158(x0, x1, True)
new_max1112(x0, x1, x2, False)
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Pos(Succ(x2))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Neg(Succ(x2))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Neg(Succ(x2))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Succ(x1)), Neg(Succ(x2))))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Pos(Succ(x2))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Succ(x1)), Pos(Succ(x2))))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Succ(x0))))
new_primMulNat2(Zero, Succ(x0))
new_max1125(x0, x1, True)
new_not1(x0, Succ(x1))
new_not8(Zero)
new_max1149(x0, x1, x2, x3, False)
new_max114(x0, x1, True)
new_max1105(x0, False)
new_max162(x0, x1, x2, True)
new_not9(Zero)
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Neg(Succ(x1))))
new_max1101(x0, x1, True)
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Succ(x0))))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Zero)))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Zero)))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Zero)))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Zero)))
new_max124(x0, x1, True)
new_max1154(x0, x1, False)
new_not7(Succ(x0))
new_max1122(x0, x1, True)
new_max1114(x0, x1, True)
new_max1(Float(Pos(Succ(x0)), Pos(Zero)), Float(Pos(Zero), Pos(Zero)))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Pos(Succ(Zero))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Pos(Succ(Zero))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Pos(Zero), Neg(Succ(Zero))), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max135(x0, x1, False)
new_max190(x0, x1, x2, False)
new_max174(x0, x1, False)
new_max112(x0, x1, True)
new_max1139(x0, False)
new_max199(x0, x1, False)
new_max130(x0, Pos(Zero), x1, Neg(Succ(x2)), Zero)
new_max1(Float(Pos(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x0))))
new_max1(Float(Neg(Zero), Neg(Zero)), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Neg(Succ(x0))))
new_max130(x0, Neg(Zero), x1, Pos(Succ(x2)), Zero)
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Pos(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Zero), Pos(Succ(x0))))
new_max156(x0, Pos(x1), x2, Pos(x3), Succ(x4))
new_max1(Float(Pos(Zero), Neg(Succ(Succ(x0)))), Float(Neg(Zero), Neg(Succ(x1))))
new_max130(x0, Neg(Zero), x1, Neg(Zero), Zero)
new_max1(Float(Neg(Succ(x0)), Neg(Succ(Succ(Succ(x1))))), Float(Neg(Zero), Neg(Succ(x2))))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Succ(x0)), Pos(Succ(x1))))
new_max161(x0)
new_max178(x0, True)
new_max1138(x0, False)
new_max163(x0, x1, False)
new_max162(x0, x1, x2, False)
new_max1110(x0, False)
new_max1136(x0, x1, False)
new_max156(x0, Neg(Succ(x1)), x2, Pos(Succ(x3)), Succ(x4))
new_max1139(x0, True)
new_max01(x0, x1, x2, x3)
new_max156(x0, Pos(Succ(x1)), x2, Neg(Succ(x3)), Succ(x4))
new_max154(x0, False)
new_max134(x0, x1, x2, True)
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Zero), Neg(Succ(x0))))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Zero))), Float(Pos(Zero), Neg(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Zero))), Float(Neg(Zero), Pos(Succ(x1))))
new_max1(Float(Pos(Succ(x0)), Neg(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x1))))
new_max1(Float(Neg(Succ(x0)), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x1))))
new_max118(x0, True)
new_max130(x0, Neg(Zero), x1, Neg(Zero), Succ(x2))
new_max1119(x0, x1, True)
new_max164(x0, x1, True)
new_max137(x0, x1, True)
new_max164(x0, x1, False)
new_max130(x0, Neg(Succ(x1)), x2, Neg(Succ(x3)), Succ(x4))
new_max1(Float(Pos(Succ(x0)), Pos(Succ(x1))), Float(Pos(Zero), Pos(Zero)))
new_max1(Float(Neg(Zero), Pos(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Neg(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Neg(Succ(x0)), Pos(Succ(x1))))
new_max1(Float(Neg(Zero), Neg(Succ(Succ(Zero)))), Float(Pos(Succ(x0)), Neg(Succ(x1))))
new_max142(x0, x1, True)
new_max130(x0, Pos(Succ(x1)), x2, Pos(Zero), Succ(x3))
new_max1126(x0, x1, False)
new_not10
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Pos(Zero), Neg(Succ(x0))))
new_max1(Float(Pos(Zero), Pos(Zero)), Float(Neg(Zero), Pos(Succ(x0))))
new_max1(Float(Neg(Zero), Pos(Zero)), Float(Pos(Zero), Pos(Succ(x0))))
new_max1(Float(Pos(Zero), Neg(Zero)), Float(Pos(Zero), Pos(Succ(x0))))
new_max198(x0, x1, True)
new_max1(Float(Pos(Succ(x0)), Pos(Succ(Zero))), Float(Pos(Zero), Pos(Succ(x1))))
new_max195(x0, x1, True)
new_max1(Float(Pos(Zero), Pos(Succ(Succ(Succ(x0))))), Float(Pos(Zero), Pos(Succ(x1))))
new_max135(x0, x1, True)
new_max1(Float(Neg(Succ(x0)), x1), Float(Neg(Succ(x2)), x3))
new_max1109(x0, False)
new_max121(x0, x1, True)
new_max152(x0, False)
new_max171(x0, x1, False)
new_max157(x0, x1, x2, True)
new_max1114(x0, x1, False)
new_max1167(x0, x1, x2, x3, True)
new_max17(x0, x1, x2, x3, True)
new_max156(x0, Pos(x1), x2, Pos(x3), Zero)
new_max1150(x0, x1, x2, False)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: